A:Type, B:(AType), f:fpf(A; a.B(a)), eq:EqDecider(A), x:A.
(fpf-dom(eq; x; f))  (fpf-ap(f; eq; x)  B(x)) 

latex

Definitions	x:A. B(x), fpf(A; a.B(a)), x(s), P  Q, fpf-dom(eq; x; f), t  T, fpf-ap(f; eq; x), x. t(x), prop{i:l}, P  Q, P  Q
Lemmas	pi2 wf, l member wf, assert wf, deq-member wf, pi1 wf, deq wf, assert-deq-member